Prädikatenlogik mit endlich vielen Variablen

Projektleitung und Mitarbeiter

Gordeew, L. (Doz. Dr. rer. nat.)

Mittelgeber :

Forschungsbericht : 1994-1996

Tel./ Fax.:

Projektbeschreibung

Prädikatenlogik mit endlich vielen Variablen wird neuartig durch einen sog. Reduktionskalkül formalisiert. Speziell ermöglicht der Reduktionskalkül ein solches algorithmisches Verfahren im prädikatenlogischen Automatischen Beweisen, das auch mit festem Variablenanzahl (im Sequenzenkalkülsinn) bzw. fester Substitutionstiefe (im Resolutionskalkülsinn) funktioniert. Im herkömmlichen Verfahren ist dies nicht der Fall.

Publikationen

Gordeev, L.: Cut free formalization of predicate logic with finitely many variables. Part I. Proc. of CSL94, Springer LN in Comp. Sci., 136 150 (1995).

INDEX HOME SUCHEN KONTAKT LINKS

qvf-info@uni-tuebingen.de(qvf-info@uni-tuebingen.de) - Stand: 30.11.96
Copyright Hinweise